$\forall$$A$, $B$:Type, $R$:($A$$\rightarrow$$A$$\rightarrow\mathbb{P}$), $S$:($B$$\rightarrow$$B$$\rightarrow\mathbb{P}$), ${\it opa}$:($A$$\rightarrow$$A$), ${\it opb}$:($B$$\rightarrow$$B$), $f$:($A$$\rightarrow$$B$).
\\[0ex]fun\_thru\_1op($A$;$B$;${\it opa}$;${\it opb}$;$f$)
\\[0ex]$\Rightarrow$ RelsIso($A$;$B$;$x$,$y$.$R$($x$,$y$);$x$,$y$.$S$($x$,$y$);$f$)
\\[0ex]$\Rightarrow$ monot($B$;$x$,$y$.$S$($x$,$y$);${\it opb}$)
\\[0ex]$\Rightarrow$ monot($A$;$x$,$y$.$R$($x$,$y$);${\it opa}$)